s, t:DSet, a, b:(:|s|  |t|). (a = b)   

latex

Up	sets 1
Definitions of Statement	DSet, a = b
Definitions	x. t(x), x f y, a = b, t  T, x:A. B(x), x(s), DSet
Lemmas	dset wf, pi2 wf, set car wf, pi1 wf, set eq wf, band wf